T:Type, L:T List, n:(||L||+1), x:T. (x  firstn(n;L))  (i:n. x = L[i]) 

latex

Definitions

{T}, Dec(P), hd(l), firstn(n;as), P  Q, ij, Unit, T, i<j, , ij, b, b, True, (x  l), P  Q, P  Q, x:A. B(x), Prop, l[i], ||as||, , A & B, {i..j}, i  j < k, AB, P & Q, A, False, P  Q, x:A. B(x), t  T

Lemmas

le wf, length wf2, select wf, int seg wf, nat wf, bnot wf, assert wf, le int wf, bool wf, lt int wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, length wf1, non neg length, length cons, l member wf, firstn wf, cons member, iff functionality wrt iff, select cons tl, decidable lt, select cons hd, decidable false, nil member